$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{B}$), $L_{1}$, $L_{2}$:$T$ List.
\\[0ex]$L_{2}$ $\leq$ filter($P$;$L_{1}$) $\Rightarrow$ ($\exists$$L_{3}$:$T$ List. $L_{3}$ $\leq$ $L_{1}$ \& $L_{2}$ $=$ filter($P$;$L_{3}$))